$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$, ${\it da}$:$k$:Knd fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$. ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$) $\in$ Type$_{\mbox{\scriptsize i'}}$